i:Id, k:Knd. hasloc(k; i)   

latex

Definitions	tt, t  T, P  Q, x:A. B(x), lnk(k), destination(l), eq_id(a; b), b, , b, A, prop{i:l}, P  Q, P  Q, Unit, hasloc(k; i), Id, Knd, isrcv(k)
Lemmas	Knd wf, Id wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, not wf, assert wf, isrcv wf, bool wf, bnot wf, eq id wf, ldst wf, lnk wf, btrue wf